Left Termination proof of /tmp/tmp38PMIl/pl8.4.2.pl

Left Termination of the query pattern e(b,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

e₂(L, T) :- t₂(L, T).
e₂(L, T) :- t₂(L, .₂(plus₀, C)), e₂(C, T).
t₂(L, T) :- n₂(L, T).
t₂(L, T) :- n₂(L, .₂(star₀, C)), t₂(C, T).
n₂(.₂(L, T), T) :- z₁(L).
n₂(.₂(lbrace₀, A), B) :- e₂(A, .₂(rbrace₀, B)).
z₁(a₀).
z₁(b₀).
z₁(c₀).

With regard to the inferred argument filtering the predicates were used in the following modes:
e₂: (b,f)
t₂: (b,f)
n₂: (b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

e_2_in_ga₂(L, T) -> if_e_2_in_1_ga₃(L, T, t_2_in_ga₂(L, T))
t_2_in_ga₂(L, T) -> if_t_2_in_1_ga₃(L, T, n_2_in_ga₂(L, T))
n_2_in_ga₂(._2₂(L, T), T) -> if_n_2_in_1_ga₃(L, T, z_1_in_g₁(L))
z_1_in_g₁(a_0) -> z_1_out_g₁(a_0)
z_1_in_g₁(b_0) -> z_1_out_g₁(b_0)
z_1_in_g₁(c_0) -> z_1_out_g₁(c_0)
if_n_2_in_1_ga₃(L, T, z_1_out_g₁(L)) -> n_2_out_ga₂(._2₂(L, T), T)
n_2_in_ga₂(._2₂(lbrace_0, A), B) -> if_n_2_in_2_ga₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
e_2_in_ga₂(L, T) -> if_e_2_in_2_ga₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
t_2_in_ga₂(L, T) -> if_t_2_in_2_ga₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
if_t_2_in_2_ga₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> if_t_2_in_3_ga₄(L, T, C, t_2_in_ga₂(C, T))
if_t_2_in_3_ga₄(L, T, C, t_2_out_ga₂(C, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_2_ga₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> if_e_2_in_3_ga₄(L, T, C, e_2_in_ga₂(C, T))
if_e_2_in_3_ga₄(L, T, C, e_2_out_ga₂(C, T)) -> e_2_out_ga₂(L, T)
if_n_2_in_2_ga₃(A, B, e_2_out_ga₂(A, ._2₂(rbrace_0, B))) -> n_2_out_ga₂(._2₂(lbrace_0, A), B)
if_t_2_in_1_ga₃(L, T, n_2_out_ga₂(L, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_1_ga₃(L, T, t_2_out_ga₂(L, T)) -> e_2_out_ga₂(L, T)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

e_2_in_ga₂(L, T) -> if_e_2_in_1_ga₃(L, T, t_2_in_ga₂(L, T))
t_2_in_ga₂(L, T) -> if_t_2_in_1_ga₃(L, T, n_2_in_ga₂(L, T))
n_2_in_ga₂(._2₂(L, T), T) -> if_n_2_in_1_ga₃(L, T, z_1_in_g₁(L))
z_1_in_g₁(a_0) -> z_1_out_g₁(a_0)
z_1_in_g₁(b_0) -> z_1_out_g₁(b_0)
z_1_in_g₁(c_0) -> z_1_out_g₁(c_0)
if_n_2_in_1_ga₃(L, T, z_1_out_g₁(L)) -> n_2_out_ga₂(._2₂(L, T), T)
n_2_in_ga₂(._2₂(lbrace_0, A), B) -> if_n_2_in_2_ga₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
e_2_in_ga₂(L, T) -> if_e_2_in_2_ga₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
t_2_in_ga₂(L, T) -> if_t_2_in_2_ga₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
if_t_2_in_2_ga₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> if_t_2_in_3_ga₄(L, T, C, t_2_in_ga₂(C, T))
if_t_2_in_3_ga₄(L, T, C, t_2_out_ga₂(C, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_2_ga₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> if_e_2_in_3_ga₄(L, T, C, e_2_in_ga₂(C, T))
if_e_2_in_3_ga₄(L, T, C, e_2_out_ga₂(C, T)) -> e_2_out_ga₂(L, T)
if_n_2_in_2_ga₃(A, B, e_2_out_ga₂(A, ._2₂(rbrace_0, B))) -> n_2_out_ga₂(._2₂(lbrace_0, A), B)
if_t_2_in_1_ga₃(L, T, n_2_out_ga₂(L, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_1_ga₃(L, T, t_2_out_ga₂(L, T)) -> e_2_out_ga₂(L, T)

E_2_IN_GA₂(L, T) -> IF_E_2_IN_1_GA₃(L, T, t_2_in_ga₂(L, T))
E_2_IN_GA₂(L, T) -> T_2_IN_GA₂(L, T)
T_2_IN_GA₂(L, T) -> IF_T_2_IN_1_GA₃(L, T, n_2_in_ga₂(L, T))
T_2_IN_GA₂(L, T) -> N_2_IN_GA₂(L, T)
N_2_IN_GA₂(._2₂(L, T), T) -> IF_N_2_IN_1_GA₃(L, T, z_1_in_g₁(L))
N_2_IN_GA₂(._2₂(L, T), T) -> Z_1_IN_G₁(L)
N_2_IN_GA₂(._2₂(lbrace_0, A), B) -> IF_N_2_IN_2_GA₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
N_2_IN_GA₂(._2₂(lbrace_0, A), B) -> E_2_IN_GA₂(A, ._2₂(rbrace_0, B))
E_2_IN_GA₂(L, T) -> IF_E_2_IN_2_GA₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
E_2_IN_GA₂(L, T) -> T_2_IN_GA₂(L, ._2₂(plus_0, C))
T_2_IN_GA₂(L, T) -> IF_T_2_IN_2_GA₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
T_2_IN_GA₂(L, T) -> N_2_IN_GA₂(L, ._2₂(star_0, C))
IF_T_2_IN_2_GA₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> IF_T_2_IN_3_GA₄(L, T, C, t_2_in_ga₂(C, T))
IF_T_2_IN_2_GA₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> T_2_IN_GA₂(C, T)
IF_E_2_IN_2_GA₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> IF_E_2_IN_3_GA₄(L, T, C, e_2_in_ga₂(C, T))
IF_E_2_IN_2_GA₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> E_2_IN_GA₂(C, T)

The TRS R consists of the following rules:

e_2_in_ga₂(L, T) -> if_e_2_in_1_ga₃(L, T, t_2_in_ga₂(L, T))
t_2_in_ga₂(L, T) -> if_t_2_in_1_ga₃(L, T, n_2_in_ga₂(L, T))
n_2_in_ga₂(._2₂(L, T), T) -> if_n_2_in_1_ga₃(L, T, z_1_in_g₁(L))
z_1_in_g₁(a_0) -> z_1_out_g₁(a_0)
z_1_in_g₁(b_0) -> z_1_out_g₁(b_0)
z_1_in_g₁(c_0) -> z_1_out_g₁(c_0)
if_n_2_in_1_ga₃(L, T, z_1_out_g₁(L)) -> n_2_out_ga₂(._2₂(L, T), T)
n_2_in_ga₂(._2₂(lbrace_0, A), B) -> if_n_2_in_2_ga₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
e_2_in_ga₂(L, T) -> if_e_2_in_2_ga₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
t_2_in_ga₂(L, T) -> if_t_2_in_2_ga₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
if_t_2_in_2_ga₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> if_t_2_in_3_ga₄(L, T, C, t_2_in_ga₂(C, T))
if_t_2_in_3_ga₄(L, T, C, t_2_out_ga₂(C, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_2_ga₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> if_e_2_in_3_ga₄(L, T, C, e_2_in_ga₂(C, T))
if_e_2_in_3_ga₄(L, T, C, e_2_out_ga₂(C, T)) -> e_2_out_ga₂(L, T)
if_n_2_in_2_ga₃(A, B, e_2_out_ga₂(A, ._2₂(rbrace_0, B))) -> n_2_out_ga₂(._2₂(lbrace_0, A), B)
if_t_2_in_1_ga₃(L, T, n_2_out_ga₂(L, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_1_ga₃(L, T, t_2_out_ga₂(L, T)) -> e_2_out_ga₂(L, T)

The argument filtering Pi contains the following mapping:
e_2_in_ga₂(x1, x2) = e_2_in_ga₁(x1)
._2₂(x1, x2) = ._2₂(x1, x2)
plus_0 = plus_0
star_0 = star_0
lbrace_0 = lbrace_0
rbrace_0 = rbrace_0
a_0 = a_0
b_0 = b_0
c_0 = c_0
if_e_2_in_1_ga₃(x1, x2, x3) = if_e_2_in_1_ga₁(x3)
t_2_in_ga₂(x1, x2) = t_2_in_ga₁(x1)
if_t_2_in_1_ga₃(x1, x2, x3) = if_t_2_in_1_ga₁(x3)
n_2_in_ga₂(x1, x2) = n_2_in_ga₁(x1)
if_n_2_in_1_ga₃(x1, x2, x3) = if_n_2_in_1_ga₂(x2, x3)
z_1_in_g₁(x1) = z_1_in_g₁(x1)
z_1_out_g₁(x1) = z_1_out_g
n_2_out_ga₂(x1, x2) = n_2_out_ga₁(x2)
if_n_2_in_2_ga₃(x1, x2, x3) = if_n_2_in_2_ga₁(x3)
if_e_2_in_2_ga₃(x1, x2, x3) = if_e_2_in_2_ga₁(x3)
if_t_2_in_2_ga₃(x1, x2, x3) = if_t_2_in_2_ga₁(x3)
if_t_2_in_3_ga₄(x1, x2, x3, x4) = if_t_2_in_3_ga₁(x4)
t_2_out_ga₂(x1, x2) = t_2_out_ga₁(x2)
if_e_2_in_3_ga₄(x1, x2, x3, x4) = if_e_2_in_3_ga₁(x4)
e_2_out_ga₂(x1, x2) = e_2_out_ga₁(x2)
IF_T_2_IN_2_GA₃(x1, x2, x3) = IF_T_2_IN_2_GA₁(x3)
IF_E_2_IN_2_GA₃(x1, x2, x3) = IF_E_2_IN_2_GA₁(x3)
IF_N_2_IN_1_GA₃(x1, x2, x3) = IF_N_2_IN_1_GA₂(x2, x3)
N_2_IN_GA₂(x1, x2) = N_2_IN_GA₁(x1)
IF_E_2_IN_1_GA₃(x1, x2, x3) = IF_E_2_IN_1_GA₁(x3)
T_2_IN_GA₂(x1, x2) = T_2_IN_GA₁(x1)
Z_1_IN_G₁(x1) = Z_1_IN_G₁(x1)
IF_N_2_IN_2_GA₃(x1, x2, x3) = IF_N_2_IN_2_GA₁(x3)
IF_T_2_IN_3_GA₄(x1, x2, x3, x4) = IF_T_2_IN_3_GA₁(x4)
E_2_IN_GA₂(x1, x2) = E_2_IN_GA₁(x1)
IF_E_2_IN_3_GA₄(x1, x2, x3, x4) = IF_E_2_IN_3_GA₁(x4)
IF_T_2_IN_1_GA₃(x1, x2, x3) = IF_T_2_IN_1_GA₁(x3)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

E_2_IN_GA₂(L, T) -> IF_E_2_IN_1_GA₃(L, T, t_2_in_ga₂(L, T))
E_2_IN_GA₂(L, T) -> T_2_IN_GA₂(L, T)
T_2_IN_GA₂(L, T) -> IF_T_2_IN_1_GA₃(L, T, n_2_in_ga₂(L, T))
T_2_IN_GA₂(L, T) -> N_2_IN_GA₂(L, T)
N_2_IN_GA₂(._2₂(L, T), T) -> IF_N_2_IN_1_GA₃(L, T, z_1_in_g₁(L))
N_2_IN_GA₂(._2₂(L, T), T) -> Z_1_IN_G₁(L)
N_2_IN_GA₂(._2₂(lbrace_0, A), B) -> IF_N_2_IN_2_GA₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
N_2_IN_GA₂(._2₂(lbrace_0, A), B) -> E_2_IN_GA₂(A, ._2₂(rbrace_0, B))
E_2_IN_GA₂(L, T) -> IF_E_2_IN_2_GA₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
E_2_IN_GA₂(L, T) -> T_2_IN_GA₂(L, ._2₂(plus_0, C))
T_2_IN_GA₂(L, T) -> IF_T_2_IN_2_GA₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
T_2_IN_GA₂(L, T) -> N_2_IN_GA₂(L, ._2₂(star_0, C))
IF_T_2_IN_2_GA₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> IF_T_2_IN_3_GA₄(L, T, C, t_2_in_ga₂(C, T))
IF_T_2_IN_2_GA₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> T_2_IN_GA₂(C, T)
IF_E_2_IN_2_GA₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> IF_E_2_IN_3_GA₄(L, T, C, e_2_in_ga₂(C, T))
IF_E_2_IN_2_GA₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> E_2_IN_GA₂(C, T)

The TRS R consists of the following rules:

e_2_in_ga₂(L, T) -> if_e_2_in_1_ga₃(L, T, t_2_in_ga₂(L, T))
t_2_in_ga₂(L, T) -> if_t_2_in_1_ga₃(L, T, n_2_in_ga₂(L, T))
n_2_in_ga₂(._2₂(L, T), T) -> if_n_2_in_1_ga₃(L, T, z_1_in_g₁(L))
z_1_in_g₁(a_0) -> z_1_out_g₁(a_0)
z_1_in_g₁(b_0) -> z_1_out_g₁(b_0)
z_1_in_g₁(c_0) -> z_1_out_g₁(c_0)
if_n_2_in_1_ga₃(L, T, z_1_out_g₁(L)) -> n_2_out_ga₂(._2₂(L, T), T)
n_2_in_ga₂(._2₂(lbrace_0, A), B) -> if_n_2_in_2_ga₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
e_2_in_ga₂(L, T) -> if_e_2_in_2_ga₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
t_2_in_ga₂(L, T) -> if_t_2_in_2_ga₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
if_t_2_in_2_ga₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> if_t_2_in_3_ga₄(L, T, C, t_2_in_ga₂(C, T))
if_t_2_in_3_ga₄(L, T, C, t_2_out_ga₂(C, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_2_ga₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> if_e_2_in_3_ga₄(L, T, C, e_2_in_ga₂(C, T))
if_e_2_in_3_ga₄(L, T, C, e_2_out_ga₂(C, T)) -> e_2_out_ga₂(L, T)
if_n_2_in_2_ga₃(A, B, e_2_out_ga₂(A, ._2₂(rbrace_0, B))) -> n_2_out_ga₂(._2₂(lbrace_0, A), B)
if_t_2_in_1_ga₃(L, T, n_2_out_ga₂(L, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_1_ga₃(L, T, t_2_out_ga₂(L, T)) -> e_2_out_ga₂(L, T)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

E_2_IN_GA₂(L, T) -> IF_E_2_IN_2_GA₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
E_2_IN_GA₂(L, T) -> T_2_IN_GA₂(L, T)
N_2_IN_GA₂(._2₂(lbrace_0, A), B) -> E_2_IN_GA₂(A, ._2₂(rbrace_0, B))
T_2_IN_GA₂(L, T) -> N_2_IN_GA₂(L, ._2₂(star_0, C))
T_2_IN_GA₂(L, T) -> IF_T_2_IN_2_GA₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
IF_E_2_IN_2_GA₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> E_2_IN_GA₂(C, T)
T_2_IN_GA₂(L, T) -> N_2_IN_GA₂(L, T)
E_2_IN_GA₂(L, T) -> T_2_IN_GA₂(L, ._2₂(plus_0, C))
IF_T_2_IN_2_GA₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> T_2_IN_GA₂(C, T)

The TRS R consists of the following rules:

e_2_in_ga₂(L, T) -> if_e_2_in_1_ga₃(L, T, t_2_in_ga₂(L, T))
t_2_in_ga₂(L, T) -> if_t_2_in_1_ga₃(L, T, n_2_in_ga₂(L, T))
n_2_in_ga₂(._2₂(L, T), T) -> if_n_2_in_1_ga₃(L, T, z_1_in_g₁(L))
z_1_in_g₁(a_0) -> z_1_out_g₁(a_0)
z_1_in_g₁(b_0) -> z_1_out_g₁(b_0)
z_1_in_g₁(c_0) -> z_1_out_g₁(c_0)
if_n_2_in_1_ga₃(L, T, z_1_out_g₁(L)) -> n_2_out_ga₂(._2₂(L, T), T)
n_2_in_ga₂(._2₂(lbrace_0, A), B) -> if_n_2_in_2_ga₃(A, B, e_2_in_ga₂(A, ._2₂(rbrace_0, B)))
e_2_in_ga₂(L, T) -> if_e_2_in_2_ga₃(L, T, t_2_in_ga₂(L, ._2₂(plus_0, C)))
t_2_in_ga₂(L, T) -> if_t_2_in_2_ga₃(L, T, n_2_in_ga₂(L, ._2₂(star_0, C)))
if_t_2_in_2_ga₃(L, T, n_2_out_ga₂(L, ._2₂(star_0, C))) -> if_t_2_in_3_ga₄(L, T, C, t_2_in_ga₂(C, T))
if_t_2_in_3_ga₄(L, T, C, t_2_out_ga₂(C, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_2_ga₃(L, T, t_2_out_ga₂(L, ._2₂(plus_0, C))) -> if_e_2_in_3_ga₄(L, T, C, e_2_in_ga₂(C, T))
if_e_2_in_3_ga₄(L, T, C, e_2_out_ga₂(C, T)) -> e_2_out_ga₂(L, T)
if_n_2_in_2_ga₃(A, B, e_2_out_ga₂(A, ._2₂(rbrace_0, B))) -> n_2_out_ga₂(._2₂(lbrace_0, A), B)
if_t_2_in_1_ga₃(L, T, n_2_out_ga₂(L, T)) -> t_2_out_ga₂(L, T)
if_e_2_in_1_ga₃(L, T, t_2_out_ga₂(L, T)) -> e_2_out_ga₂(L, T)

The argument filtering Pi contains the following mapping:
e_2_in_ga₂(x1, x2) = e_2_in_ga₁(x1)
._2₂(x1, x2) = ._2₂(x1, x2)
plus_0 = plus_0
star_0 = star_0
lbrace_0 = lbrace_0
rbrace_0 = rbrace_0
a_0 = a_0
b_0 = b_0
c_0 = c_0
if_e_2_in_1_ga₃(x1, x2, x3) = if_e_2_in_1_ga₁(x3)
t_2_in_ga₂(x1, x2) = t_2_in_ga₁(x1)
if_t_2_in_1_ga₃(x1, x2, x3) = if_t_2_in_1_ga₁(x3)
n_2_in_ga₂(x1, x2) = n_2_in_ga₁(x1)
if_n_2_in_1_ga₃(x1, x2, x3) = if_n_2_in_1_ga₂(x2, x3)
z_1_in_g₁(x1) = z_1_in_g₁(x1)
z_1_out_g₁(x1) = z_1_out_g
n_2_out_ga₂(x1, x2) = n_2_out_ga₁(x2)
if_n_2_in_2_ga₃(x1, x2, x3) = if_n_2_in_2_ga₁(x3)
if_e_2_in_2_ga₃(x1, x2, x3) = if_e_2_in_2_ga₁(x3)
if_t_2_in_2_ga₃(x1, x2, x3) = if_t_2_in_2_ga₁(x3)
if_t_2_in_3_ga₄(x1, x2, x3, x4) = if_t_2_in_3_ga₁(x4)
t_2_out_ga₂(x1, x2) = t_2_out_ga₁(x2)
if_e_2_in_3_ga₄(x1, x2, x3, x4) = if_e_2_in_3_ga₁(x4)
e_2_out_ga₂(x1, x2) = e_2_out_ga₁(x2)
IF_T_2_IN_2_GA₃(x1, x2, x3) = IF_T_2_IN_2_GA₁(x3)
IF_E_2_IN_2_GA₃(x1, x2, x3) = IF_E_2_IN_2_GA₁(x3)
N_2_IN_GA₂(x1, x2) = N_2_IN_GA₁(x1)
T_2_IN_GA₂(x1, x2) = T_2_IN_GA₁(x1)
E_2_IN_GA₂(x1, x2) = E_2_IN_GA₁(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

E_2_IN_GA₁(L) -> IF_E_2_IN_2_GA₁(t_2_in_ga₁(L))
E_2_IN_GA₁(L) -> T_2_IN_GA₁(L)
N_2_IN_GA₁(._2₂(lbrace_0, A)) -> E_2_IN_GA₁(A)
T_2_IN_GA₁(L) -> N_2_IN_GA₁(L)
T_2_IN_GA₁(L) -> IF_T_2_IN_2_GA₁(n_2_in_ga₁(L))
IF_E_2_IN_2_GA₁(t_2_out_ga₁(._2₂(plus_0, C))) -> E_2_IN_GA₁(C)
IF_T_2_IN_2_GA₁(n_2_out_ga₁(._2₂(star_0, C))) -> T_2_IN_GA₁(C)

The TRS R consists of the following rules:

e_2_in_ga₁(L) -> if_e_2_in_1_ga₁(t_2_in_ga₁(L))
t_2_in_ga₁(L) -> if_t_2_in_1_ga₁(n_2_in_ga₁(L))
n_2_in_ga₁(._2₂(L, T)) -> if_n_2_in_1_ga₂(T, z_1_in_g₁(L))
z_1_in_g₁(a_0) -> z_1_out_g
z_1_in_g₁(b_0) -> z_1_out_g
z_1_in_g₁(c_0) -> z_1_out_g
if_n_2_in_1_ga₂(T, z_1_out_g) -> n_2_out_ga₁(T)
n_2_in_ga₁(._2₂(lbrace_0, A)) -> if_n_2_in_2_ga₁(e_2_in_ga₁(A))
e_2_in_ga₁(L) -> if_e_2_in_2_ga₁(t_2_in_ga₁(L))
t_2_in_ga₁(L) -> if_t_2_in_2_ga₁(n_2_in_ga₁(L))
if_t_2_in_2_ga₁(n_2_out_ga₁(._2₂(star_0, C))) -> if_t_2_in_3_ga₁(t_2_in_ga₁(C))
if_t_2_in_3_ga₁(t_2_out_ga₁(T)) -> t_2_out_ga₁(T)
if_e_2_in_2_ga₁(t_2_out_ga₁(._2₂(plus_0, C))) -> if_e_2_in_3_ga₁(e_2_in_ga₁(C))
if_e_2_in_3_ga₁(e_2_out_ga₁(T)) -> e_2_out_ga₁(T)
if_n_2_in_2_ga₁(e_2_out_ga₁(._2₂(rbrace_0, B))) -> n_2_out_ga₁(B)
if_t_2_in_1_ga₁(n_2_out_ga₁(T)) -> t_2_out_ga₁(T)
if_e_2_in_1_ga₁(t_2_out_ga₁(T)) -> e_2_out_ga₁(T)

The set Q consists of the following terms:

e_2_in_ga₁(x0)
t_2_in_ga₁(x0)
n_2_in_ga₁(x0)
z_1_in_g₁(x0)
if_n_2_in_1_ga₂(x0, x1)
if_t_2_in_2_ga₁(x0)
if_t_2_in_3_ga₁(x0)
if_e_2_in_2_ga₁(x0)
if_e_2_in_3_ga₁(x0)
if_n_2_in_2_ga₁(x0)
if_t_2_in_1_ga₁(x0)
if_e_2_in_1_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_E_2_IN_2_GA₁, E_2_IN_GA₁, T_2_IN_GA₁, N_2_IN_GA₁, IF_T_2_IN_2_GA₁}.
We used the following order together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Polynomial interpretation:

POL(a_0) = 0
POL(rbrace_0) = 0
POL(c_0) = 0
POL(n_2_out_ga₁(x₁)) = x₁
POL(star_0) = 1
POL(e_2_in_ga₁(x₁)) = x₁
POL(if_t_2_in_2_ga₁(x₁)) = x₁
POL(if_e_2_in_3_ga₁(x₁)) = x₁
POL(plus_0) = 1
POL(t_2_in_ga₁(x₁)) = x₁
POL(if_n_2_in_1_ga₂(x₁, x₂)) = x₁
POL(._2₂(x₁, x₂)) = 1 + x₂
POL(n_2_in_ga₁(x₁)) = x₁
POL(z_1_in_g₁(x₁)) = 0
POL(t_2_out_ga₁(x₁)) = x₁
POL(if_e_2_in_1_ga₁(x₁)) = x₁
POL(if_n_2_in_2_ga₁(x₁)) = x₁
POL(if_e_2_in_2_ga₁(x₁)) = x₁
POL(if_t_2_in_1_ga₁(x₁)) = x₁
POL(e_2_out_ga₁(x₁)) = x₁
POL(if_t_2_in_3_ga₁(x₁)) = x₁
POL(b_0) = 0
POL(z_1_out_g) = 0
POL(lbrace_0) = 1

From the DPs we obtained the following set of size-change graphs:

IF_E_2_IN_2_GA₁(t_2_out_ga₁(._2₂(plus_0, C))) -> E_2_IN_GA₁(C) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1
N_2_IN_GA₁(._2₂(lbrace_0, A)) -> E_2_IN_GA₁(A) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1
T_2_IN_GA₁(L) -> N_2_IN_GA₁(L) (allowed arguments on rhs = {1})
The graph contains the following edges 1 >= 1
T_2_IN_GA₁(L) -> IF_T_2_IN_2_GA₁(n_2_in_ga₁(L)) (allowed arguments on rhs = {1})
The graph contains the following edges 1 >= 1
IF_T_2_IN_2_GA₁(n_2_out_ga₁(._2₂(star_0, C))) -> T_2_IN_GA₁(C) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1
E_2_IN_GA₁(L) -> T_2_IN_GA₁(L) (allowed arguments on rhs = {1})
The graph contains the following edges 1 >= 1
E_2_IN_GA₁(L) -> IF_E_2_IN_2_GA₁(t_2_in_ga₁(L)) (allowed arguments on rhs = {1})
The graph contains the following edges 1 >= 1

We oriented the following set of usable rules.

t_2_in_ga₁(L) -> if_t_2_in_2_ga₁(n_2_in_ga₁(L))
t_2_in_ga₁(L) -> if_t_2_in_1_ga₁(n_2_in_ga₁(L))
n_2_in_ga₁(._2₂(L, T)) -> if_n_2_in_1_ga₂(T, z_1_in_g₁(L))
n_2_in_ga₁(._2₂(lbrace_0, A)) -> if_n_2_in_2_ga₁(e_2_in_ga₁(A))
if_t_2_in_3_ga₁(t_2_out_ga₁(T)) -> t_2_out_ga₁(T)
if_t_2_in_2_ga₁(n_2_out_ga₁(._2₂(star_0, C))) -> if_t_2_in_3_ga₁(t_2_in_ga₁(C))
if_t_2_in_1_ga₁(n_2_out_ga₁(T)) -> t_2_out_ga₁(T)
if_n_2_in_2_ga₁(e_2_out_ga₁(._2₂(rbrace_0, B))) -> n_2_out_ga₁(B)
if_n_2_in_1_ga₂(T, z_1_out_g) -> n_2_out_ga₁(T)
if_e_2_in_3_ga₁(e_2_out_ga₁(T)) -> e_2_out_ga₁(T)
if_e_2_in_2_ga₁(t_2_out_ga₁(._2₂(plus_0, C))) -> if_e_2_in_3_ga₁(e_2_in_ga₁(C))
if_e_2_in_1_ga₁(t_2_out_ga₁(T)) -> e_2_out_ga₁(T)
e_2_in_ga₁(L) -> if_e_2_in_2_ga₁(t_2_in_ga₁(L))
e_2_in_ga₁(L) -> if_e_2_in_1_ga₁(t_2_in_ga₁(L))